Lean 4 基礎 - pogi-log

Lean 4 基礎

Lean 4のドキュメント

What is Lean - Lean Manual

Theorem Proving in Lean 4 - Theorem Proving in Lean 4

Theorem Proving in Lean 4 日本語訳 - Theorem Proving in Lean 4 日本語訳

コメント

code:memo

-- 1行コメント

/-

複数行コメント

-/

宣言的コマンド

#で始まるものは実行すると結果がすぐに確認できるようコマンドに分類される

こういうのは「対話的」とよばれる

code:memo

-- evalコマンド

#eval "Hello, World!"

--> "Hello, World!"

def double (x : Nat) : Nat :=

x + x

#eval double 3

--> 6

code:memo

-- #check コマンド

#check 2 + 2 = 4

--> 2 + 2 = 4 : Prop

code:memo

theorem easy : 2 + 2 = 4 :=

rfl

theorem hard : FermatLastTheorem :=

sorry

uは宇宙レベルを表す変数

タクティク

証明を書くためのコマンドはタクティク(tactic)

rw

rfl

apply

induction

rw

⊢

Goalが左辺=右辺なら証明完了

induction n with d hd

apply

含意 → を適用するタクティク

apply h2 at h1なら仮定h2を仮定h1に適用する

code:memo

h1: x = 37

h2: x = 37 → y = 42

↓ apply h2 at h1

h2: x = 37 → y = 42

h1: y = 42

apply succ_inj at hなら仮定hのsuccを除去する

succ(a) = succ(b)→a = b

code:memo

h: succ (succ 0) = succ (succ (succ 0))

↓ apply succ_inj at h

h: succ 0 = succ (succ 0)

apply succ_injならゴールに適用する

exact

exact hで仮定とゴールを比較する

数学系のためのLean勉強会 - 数学系のためのLean勉強会

【Lean実況】数学系のためのLean勉強会の教材を解くBasic1 - YouTube

https://www.youtube.com/watch?v=1saX8G-wN2o&list=PL-2TwNpShL3yJRE2xUwOEujUv6j4S0_ml&index=1

確認用

Q. 1行コメント

Q. 複数行コメント

Q. intro

Q. constructor

Q. cases

Q. rw

Q. apply

Q. simp

Q. exact

参考

依存型理論 - Theorem Proving in Lean 4 日本語訳

タクティク - Lean by Example

数学系のためのLean勉強会 - 数学系のためのLean勉強会

Leanのインストール・基礎

関連

単純型理論

依存型理論

Types as objects

Proj: Natural number gameを解く

メモ

GitHub: yuma-mizuno/lean-math-workshop: 数学系のためのLean勉強会

証明支援システムLeanに入門する #2

調査用

/pogi-log/Google.icon Lean 4 基礎